\relax 
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\citation{WTS2001}
\citation{BCJ2001}
\citation{KPJ2005}
\citation{DOG2001}
\citation{CJG2001}
\citation{KPS2005}
\citation{WTS2001}
\citation{MM2005}
\citation{ZWR2003}
\citation{ZWL2005}
\citation{Z11}
\citation{Jan10}
\citation{MINISAT}
\citation{MK2002}
\citation{RSF2004}
\citation{Z11}
\citation{JLM15}
\citation{MINISAT}
\@writefile{toc}{\contentsline {section}{Introduction}{1}{section*.1}}
\citation{JLM15}
\citation{Jan10}
\@writefile{toc}{\contentsline {section}{Preliminaries}{2}{section*.2}}
\newlabel{sec:prel}{{}{2}{Preliminaries\relax }{section*.2}{}}
\newlabel{def:backbone}{{1}{2}{Backbone\relax }{definition.1}{}}
\newlabel{thm:co-NP}{{1}{2}{\relax }{theorem.1}{}}
\@writefile{toc}{\contentsline {section}{Overview of Our Approach}{2}{section*.3}}
\newlabel{sec:walg}{{}{2}{Overview of Our Approach\relax }{section*.3}{}}
\citation{LMZ09}
\citation{LMZ09}
\citation{Par03}
\citation{LMZ09}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Overview of our approach}}{3}{figure.1}}
\newlabel{flow}{{1}{3}{Overview of our approach\relax }{figure.1}{}}
\@writefile{toc}{\contentsline {section}{Computing $\overline  {\textsf  {BL}}_u(\Phi )$}{3}{section*.4}}
\@writefile{toc}{\contentsline {subsection}{An Na\"{\i }ve Algorithm}{4}{section*.5}}
\@writefile{loa}{\contentsline {algocf}{\numberline {1}{\ignorespaces Non-backbones under-approximation}}{4}{algocf.1}}
\newlabel{alg:no-loop-w}{{1}{4}{An Na\"{\i }ve Algorithm\relax }{algocf.1}{}}
\newlabel{lem:nBL}{{6}{4}{An Na\"{\i }ve Algorithm\relax }{lemma.1}{}}
\@writefile{toc}{\contentsline {subsection}{Heuristic-based Algorithm}{4}{section*.6}}
\@writefile{loa}{\contentsline {algocf}{\numberline {2}{\ignorespaces Heuristic extension for computing $\overline  {\textsf  {BL}}_u$}}{5}{algocf.2}}
\newlabel{alg:whiten-greedy}{{2}{5}{Heuristic-based Algorithm\relax }{algocf.2}{}}
\newlabel{alg:wal}{{2}{5}{Heuristic-based Algorithm\relax }{algocf.2}{}}
\@writefile{toc}{\contentsline {section}{Computing ${\sf  HBL}\xspace  (\Phi )$}{5}{section*.7}}
\@writefile{loa}{\contentsline {algocf}{\numberline {3}{\ignorespaces Backbones Estimation of $\Phi $, $\textsf  {HDBS}\xspace  (\Phi )$}}{5}{algocf.3}}
\newlabel{alg:nBLo}{{3}{5}{Computing $\HBL (\Phi )$\relax }{algocf.3}{}}
\citation{MINISAT}
\@writefile{loa}{\contentsline {algocf}{\numberline {4}{\ignorespaces Backbones Extracting Using MUC}}{6}{algocf.4}}
\newlabel{alg:MUC}{{4}{6}{Computing $\HBL (\Phi )$\relax }{algocf.4}{}}
\@writefile{toc}{\contentsline {section}{Experiments results}{6}{section*.8}}
\newlabel{sec:expr}{{13}{6}{Experiments results\relax }{section*.8}{}}
\citation{JLM15}
\citation{MPA2015}
\@writefile{toc}{\contentsline {subsection}{Experimental Strategies}{7}{section*.9}}
\@writefile{toc}{\contentsline {subsection}{MSS Extraction Experimental Results}{7}{section*.10}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Total time use for formulae from MCS computing}}{7}{figure.2}}
\newlabel{fig:mcs-time}{{2}{7}{Total time use for formulae from MCS computing\relax }{figure.2}{}}
\@writefile{toc}{\contentsline {subsection}{Industrial Experimental Results}{7}{section*.11}}
\bibstyle{aaai}
\bibdata{bib}
\bibcite{BCJ2001}{\citeauthoryear {Bollob{\'a}s \bgroup et al\unhbox \voidb@x \hbox {.}\egroup }{2001}}
\bibcite{CJG2001}{\citeauthoryear {Culberson and Gent}{2001}}
\bibcite{DOG2001}{\citeauthoryear {Dubois and Dequen}{2001}}
\bibcite{MINISAT}{\citeauthoryear {Eén and Sörensson}{2004}}
\bibcite{JLM15}{\citeauthoryear {Janota, Lynce, and Marques{-}Silva}{2015}}
\bibcite{Jan10}{\citeauthoryear {Janota}{2010}}
\bibcite{KPJ2005}{\citeauthoryear {Kilby \bgroup et al\unhbox \voidb@x \hbox {.}\egroup }{2005a}}
\bibcite{KPS2005}{\citeauthoryear {Kilby \bgroup et al\unhbox \voidb@x \hbox {.}\egroup }{2005b}}
\bibcite{LMZ09}{\citeauthoryear {Li, Ma, and Zhou}{2009}}
\bibcite{MK2002}{\citeauthoryear {McMillan}{2002}}
\bibcite{MM2005}{\citeauthoryear {Mena{\"\i }}{2005}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Total time use for formulae from industrial}}{8}{figure.3}}
\newlabel{fig:ind-time}{{3}{8}{Total time use for formulae from industrial\relax }{figure.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Total SAT calls number for fixed percentages of backbones formulae}}{8}{figure.4}}
\newlabel{fig:fix}{{4}{8}{Total SAT calls number for fixed percentages of backbones formulae\relax }{figure.4}{}}
\@writefile{toc}{\contentsline {subsection}{Fixed Percentage Experiments Results}{8}{section*.12}}
\@writefile{toc}{\contentsline {section}{Conclusion}{8}{section*.13}}
\newlabel{sec:conc}{{13}{8}{Conclusion\relax }{section*.13}{}}
\bibcite{MPA2015}{\citeauthoryear {Menc{\i }a, Previti, and Marques-Silva}{2015}}
\bibcite{Par03}{\citeauthoryear {Parisi}{2003}}
\bibcite{RSF2004}{\citeauthoryear {Ravi and Somenzi}{2004}}
\bibcite{WTS2001}{\citeauthoryear {Walsh and Slaney}{2001}}
\bibcite{ZWL2005}{\citeauthoryear {Zhang and Looks}{2005}}
\bibcite{ZWR2003}{\citeauthoryear {Zhang, Rangan, and Looks}{2003}}
\bibcite{Z11}{\citeauthoryear {Zhu \bgroup et al\unhbox \voidb@x \hbox {.}\egroup }{2011}}
